Nuprl Lemma : comb_for_select_wf
2,24
postcript
pdf
(
A
,
l
,
n
,
z
.
l
[
n
])
A
:Type
l
:(
A
List)
n
:
(0
n
&
n
<||
l
||)
A
latex
Definitions
t
T
,
x
:
A
.
B
(
x
)
,
||
as
||
,
Prop
,
A
B
,
P
&
Q
,
T
,
P
Q
Lemmas
select
wf
,
squash
wf
,
le
wf
,
length
wf1
origin
A,l,n,z. l[n]) 
A:Type
l:(A List)n:
(0
n & n<||l||)A A,l,n,z. l[n]) A:Typel:(A List)n:(0n & n<||l||)A T
x:A. B(x)BT
Q